(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () String)
(declare-fun f () String)
(declare-fun g () String)
(declare-fun h () String)
(declare-fun i () String)
(declare-fun j () String)
(declare-fun k () String)
(declare-fun l () Int)
(declare-fun m () Bool)
(declare-fun n () Int)
(assert (distinct "" k))
(assert (= m (distinct c (- 1))))
(assert (ite m (and (= c b) (= k g) (= b (str.len e)) (= g "abcd") (not (str.in.re j (re.inter (str.to.re "") (str.to.re "a"))))) (distinct d 1)))
(assert (= l (+ c 8) n l))
(assert (= a (div d n)))
(assert (>= d n))
(assert (= a (str.len f)))
(assert (= k (str.++ h f i)))
(check-sat)
